Nuprl Lemma : es-is-interface-restrict2
11,40
postcript
pdf
A
:Type,
es
:ES,
I
:AbsInterface(
A
),
P
:(E
),
p
:(
e
:E. Dec(
P
(
e
))),
e
:E.
(
(
e
(
I
|
p
)))
(
(
e
I
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
b
,
P
Q
,
f
(
a
)
,
x
(
s
)
,
Dec(
P
)
,
Type
,
,
AbsInterface(
A
)
,
ES
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
es-is-interface-restrict
,
es-E
wf
origin
A:Type, es:ES, I:AbsInterface(A), P:(E
), p:(e:E. Dec(P(e))), e:E.
(e 
(I|p))) 
((e I)) A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
(e (I|p))) ((e I)) Tx:A. B(x)B(x)b Q
Q Q